Inference at * 2 1 1 1 
Iof proof for Lemma p-fun-exp-compose:



1. T : Type
2. n : 
3. 0 < n
4. h, f:(T(T + Top)). f^n - 1 o h   = primrec(n - 1;h;i,g. f o g  )
5. T(T + Top)
6. f : T(T + Top)
7. id : T(T + Top)
8. p-id() = id
  primrec(1+(n - 1);id;i,g. f o g  ) = f o primrec(n - 1;id;i,g. f o g  )   

latex

 by RWO "primrec_add" 0 THEN Auto THEN Reduce 0 THEN Auto 

latex

 .

Definitions	P  Q, P & Q, x:A  B(x), P  Q, , #$n, , {x:A| B(x)} , A, False, P  Q, Void, a < b, A  B, x.A(x), {i..j}, n+m, f o g  , t  T, primrec(n;b;c), x:A. B(x), s = t, x:AB(x), left + right, Top
Lemmas	primrec add, le wf, int seg wf, p-compose wf, primrec wf